FDL - Nuprl Lemma : es-interface-le-pred-bool

Nuprl Lemma : es-interface-le-pred-bool

es:ES, P:(E

).

X:AbsInterface(E)

(

e:E.

((

(e

X))

(

a:E. (es-p-le-pred(es;

e.

(P(e)))(e,a))))

& ((

(e

X))

(es-p-le-pred(es;

e.

(P(e)))(e,X(e)))))

Definitions Dec(P), x:AB(x), x:A. B(x), b, s = t, P Q, x:A B(x), x:A. B(x), b | a, a ~ b, a b, a <p b, a < b, A c B, f(a), x f y, xL. P(x), (xL.P(x)), r s, r < s, q-rel(r;x), Outcome, (x l), l_disjoint(T;l1;l2), (e <loc e'), e loc e' , (e < e'), e c e', e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), ES, E, t T, strong-subtype(A;B), left + right, P Q, P & Q, False, A, P Q, a < b, A B, x.A(x), , Type, , AbsInterface(A), es-p-le-pred(es;P)

Lemmas es-p-le-pred wf, iff wf, es-interface wf, bool wf, event system wf, es-interface-le-pred, es-E wf, assert wf, decidable wf, decidable assert